This already in the library as equiv-is-empty. Note that any map into the empty type (or indeed into any empty type) is an equivalence.

A few pointers:

• Any proposition equipped with an element is contractible. This is shown here: is-proof-irrelevant-is-prop. The notion of proof irrelevance means A -> is-contr A in agda-unimath.
• Any contractible type is equivalent to the unit type: equiv-unit-is-contr.

Nice!

Would you mind renaming this to comp-injection? This would fit better with the naming scheme we currently have, which goes comp-pointed-map, comp-hom-Group, and so on.

Note that I just found an exception to this naming scheme, which is that we use equiv-comp. That's probably a mistake on our part, which we missed because we usually use the infix notation for composition of equivalences.

Would you mind renaming this file to transitive-closures-binary-relations?

We usually name the concept of interest first, and then disambiguate later. For instance, we have several files about the action on identifications files all named action-on-identifications-disambiguation.

I would make "Formulas" the first word, so that it doesn't confuse people that something starting with the "M" is listed among the files starting with "F" in an otherwise alphabetically ordered list.

I would place this under ## Properties

I would make the first word of this title "Deductions" so that it starts with the D, because the file titles will be listed by the file names in alphabetic ordering.

A sentence explaining this definition informally would be nice. For instance:

We try to avoid modules that cross over sections, just because it is harder for the reader to keep track of what is assumed and sections seem a natural breaking point. This approach requires the arguments to be given a few more times, but we find it improves readability.

It also improves maintainability to break modules more often, because it is easier to move code around if it's not in a module that spans a large portion of the file.

I would also suggest:

• Renaming modal-logic-closure to deductive-closure-modal-theory
• Adding an entry is-in-deductive-closure-modal-theory instead of using is-in-subtype (modal-logic-closure theory) later on.

If my previous renaming suggestions are accepted, then this one could be named is-in-deductive-closure-is-in-modal-theory.

It would make sense if the consistent and inconsistent modal theories each get their own sections ### Inconsistent modal theories and ### Consistent modal theories.

I would name this is-inconsistent-modal-theory-Prop, and the next one is-inconsistent-modal-theory.

The point is that it is a predicate on modal theories, which isn't currently reflected in the name. I personally find inconsistent reading a bit better than contradictory, and it is also more consistent with your use of consistent of the name for consistent modal theories.

I would also put this in a new section.

One question I have about your definition of contradictory modal logics is that currently it says that a theory is contradictory if it contains falsehood. However, theories are not deductively closed, so wouldn't it be more natural to say that modal theories are inconsistent if their deductive closure contains falsehood?

However, theories are not deductively closed, so wouldn't it be more natural to say that modal theories are inconsistent if their deductive closure contains falsehood?

On the one hand, this would be correct from a definitional point of view. But on the other hand, in proofs this definition is already used in relation to closures, therefore it is convenient to use it in this form. I'll think about how best to determine

I don't wish to dogpile on you, but I noticed this one while browsing through the code and thought you might not know about it. Agda implements pattern-matching in module declarations and type declarations via let-bindings. These don't interact well with Agda's interactive mode, leading to unreadable goal expressions down the line. Therefore we advise against using pattern matching in places such as this one. The principled approach is to define named projection maps for propositional resizing and then use those instead.

Oh, ok, I will fix this. I agree, It's really hard to read in interactive mode

A better name for this will be left-inclusion-intersection-subtype. Note that we build our names exactly the other way around: We first state the name of the operation left-inclusion and then disambiguate it by intersection-subtype.

A better name for this will be right-inclusion-intersection-subtype

Maybe a better name would be inclusion-intersection-inclusion-subtype, which would read as the inclusion in the intersection obtained from the inclusion(s) into the subtypes.

Perhaps there are even better suggestions.

This would say that intersection is an idempotent operation, so perhaps is-idempotent-intersection-subtype would be a more descriptive name.

See also https://en.wikipedia.org/wiki/Idempotence

I would call this inclusion-is-commutative-intersection-subtype

I would call this in-concat-list-in-right-list.

This one is more tricky to name, but in-concat-list reads too much like the predicate "to be in a concatenated list". Perhaps we could consider calling it cases-in-concat-list.

I think this entry is fine in this file.

Given what this function does, perhaps map-element-list is more descriptive. Feel free to disregard this suggestion, if you think dependent-map-list is better.

Perhaps the "image" of a list would be a good name for this concept. What you describe here is equivalent to the image of the projection map

  (Sigma (a : A), a ∈ l) → A

where the first time is the type of all elements of l. If you agree with this suggestion, we could change the file name to images-lists.lagda.md and the title to # Images of lists.

For the ## Idea section, I have the following suggestion:

Changing the concept name to "image of lists" would also trigger some name changes in your entries below. The basic name would be image-list. Let me know if you want me to go through all of them and make suggestions, or whether you like to come up with names yourself.

This operation takes an injective map and returns a modal theory. Perhaps an informal sentence explaining this would be helpful. A few things to note: For this construction to work, h could be any injection X → modal-formula i where X is an arbitrary type. This observation leads me to think that a more descriptive name for this construction would be modal-theory-injection-modal-formula, to say that it is the modal theory obtained from an injection into the type of modal formulas.

One thing to note is that we have a lot more infrastructure for embeddings than for injective maps. A map between sets is injective if and only if it is an embedding, but because the concept of embeddings is better behaved for arbitrary types (types that are not sets), we generally prefer to work with embeddings.

For instance, the fact that any embedding induces a subtype is in the library as fiber-emb-Prop. Admittedly, this name is rather cryptic and could be improved on our part (a better name would be subtype-emb).

The fact that injective maps between sets are embeddings is is-emb-is-injective, and the fact that injective maps between sets are propositional maps is is-prop-map-is-injective.

Your construction here is essentially combining those constructions without referring to them, so it would be better to use them explicitly.

I wouldn't ask you to change your current approach, which is absolutely fine, but it could be even better if you tried using embeddings more. One benefit of using embeddings is that a potential future generalization to modal theories with an arbitrary type of variables could be easier. We could be less reliant on the fact that modal theories are sets.

One further minor difference between the fibers of an embedding and your type Σ (modal-formula i) (λ a → f ＝ h a), is that your type is fiber' h f, where fiber' can be found here. In general, it is good to use existing definitions, so that you can also use the existing infrastructure for those definitions. In this case I would also suggest that using fiber would be better than using fiber', because the library has a lot more stuff about the main definition of fibers.

Given the previous discussion, perhaps modal-theory-injection-pair-modal-formula could be more descriptive? It would describe the modal theory obtained from the injection of pairs of modal formulas.